0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 0 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 11 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 14 ms)
↳12 QDP
↳13 QDPSizeChangeProof (⇔, 0 ms)
↳14 YES
flB_in_gaa([], [], 0) → flB_out_gaa([], [], 0)
flB_in_gaa(.(T8, T9), T12, s(T13)) → U3_gaa(T8, T9, T12, T13, pA_in_gaaga(T8, X13, T12, T9, T13))
pA_in_gaaga([], T19, T19, T9, T20) → U1_gaaga(T19, T9, T20, flB_in_gaa(T9, T19, T20))
U1_gaaga(T19, T9, T20, flB_out_gaa(T9, T19, T20)) → pA_out_gaaga([], T19, T19, T9, T20)
pA_in_gaaga(.(T27, T28), X38, .(T27, T30), T9, T31) → U2_gaaga(T27, T28, X38, T30, T9, T31, pA_in_gaaga(T28, X38, T30, T9, T31))
U2_gaaga(T27, T28, X38, T30, T9, T31, pA_out_gaaga(T28, X38, T30, T9, T31)) → pA_out_gaaga(.(T27, T28), X38, .(T27, T30), T9, T31)
U3_gaa(T8, T9, T12, T13, pA_out_gaaga(T8, X13, T12, T9, T13)) → flB_out_gaa(.(T8, T9), T12, s(T13))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
flB_in_gaa([], [], 0) → flB_out_gaa([], [], 0)
flB_in_gaa(.(T8, T9), T12, s(T13)) → U3_gaa(T8, T9, T12, T13, pA_in_gaaga(T8, X13, T12, T9, T13))
pA_in_gaaga([], T19, T19, T9, T20) → U1_gaaga(T19, T9, T20, flB_in_gaa(T9, T19, T20))
U1_gaaga(T19, T9, T20, flB_out_gaa(T9, T19, T20)) → pA_out_gaaga([], T19, T19, T9, T20)
pA_in_gaaga(.(T27, T28), X38, .(T27, T30), T9, T31) → U2_gaaga(T27, T28, X38, T30, T9, T31, pA_in_gaaga(T28, X38, T30, T9, T31))
U2_gaaga(T27, T28, X38, T30, T9, T31, pA_out_gaaga(T28, X38, T30, T9, T31)) → pA_out_gaaga(.(T27, T28), X38, .(T27, T30), T9, T31)
U3_gaa(T8, T9, T12, T13, pA_out_gaaga(T8, X13, T12, T9, T13)) → flB_out_gaa(.(T8, T9), T12, s(T13))
FLB_IN_GAA(.(T8, T9), T12, s(T13)) → U3_GAA(T8, T9, T12, T13, pA_in_gaaga(T8, X13, T12, T9, T13))
FLB_IN_GAA(.(T8, T9), T12, s(T13)) → PA_IN_GAAGA(T8, X13, T12, T9, T13)
PA_IN_GAAGA([], T19, T19, T9, T20) → U1_GAAGA(T19, T9, T20, flB_in_gaa(T9, T19, T20))
PA_IN_GAAGA([], T19, T19, T9, T20) → FLB_IN_GAA(T9, T19, T20)
PA_IN_GAAGA(.(T27, T28), X38, .(T27, T30), T9, T31) → U2_GAAGA(T27, T28, X38, T30, T9, T31, pA_in_gaaga(T28, X38, T30, T9, T31))
PA_IN_GAAGA(.(T27, T28), X38, .(T27, T30), T9, T31) → PA_IN_GAAGA(T28, X38, T30, T9, T31)
flB_in_gaa([], [], 0) → flB_out_gaa([], [], 0)
flB_in_gaa(.(T8, T9), T12, s(T13)) → U3_gaa(T8, T9, T12, T13, pA_in_gaaga(T8, X13, T12, T9, T13))
pA_in_gaaga([], T19, T19, T9, T20) → U1_gaaga(T19, T9, T20, flB_in_gaa(T9, T19, T20))
U1_gaaga(T19, T9, T20, flB_out_gaa(T9, T19, T20)) → pA_out_gaaga([], T19, T19, T9, T20)
pA_in_gaaga(.(T27, T28), X38, .(T27, T30), T9, T31) → U2_gaaga(T27, T28, X38, T30, T9, T31, pA_in_gaaga(T28, X38, T30, T9, T31))
U2_gaaga(T27, T28, X38, T30, T9, T31, pA_out_gaaga(T28, X38, T30, T9, T31)) → pA_out_gaaga(.(T27, T28), X38, .(T27, T30), T9, T31)
U3_gaa(T8, T9, T12, T13, pA_out_gaaga(T8, X13, T12, T9, T13)) → flB_out_gaa(.(T8, T9), T12, s(T13))
FLB_IN_GAA(.(T8, T9), T12, s(T13)) → U3_GAA(T8, T9, T12, T13, pA_in_gaaga(T8, X13, T12, T9, T13))
FLB_IN_GAA(.(T8, T9), T12, s(T13)) → PA_IN_GAAGA(T8, X13, T12, T9, T13)
PA_IN_GAAGA([], T19, T19, T9, T20) → U1_GAAGA(T19, T9, T20, flB_in_gaa(T9, T19, T20))
PA_IN_GAAGA([], T19, T19, T9, T20) → FLB_IN_GAA(T9, T19, T20)
PA_IN_GAAGA(.(T27, T28), X38, .(T27, T30), T9, T31) → U2_GAAGA(T27, T28, X38, T30, T9, T31, pA_in_gaaga(T28, X38, T30, T9, T31))
PA_IN_GAAGA(.(T27, T28), X38, .(T27, T30), T9, T31) → PA_IN_GAAGA(T28, X38, T30, T9, T31)
flB_in_gaa([], [], 0) → flB_out_gaa([], [], 0)
flB_in_gaa(.(T8, T9), T12, s(T13)) → U3_gaa(T8, T9, T12, T13, pA_in_gaaga(T8, X13, T12, T9, T13))
pA_in_gaaga([], T19, T19, T9, T20) → U1_gaaga(T19, T9, T20, flB_in_gaa(T9, T19, T20))
U1_gaaga(T19, T9, T20, flB_out_gaa(T9, T19, T20)) → pA_out_gaaga([], T19, T19, T9, T20)
pA_in_gaaga(.(T27, T28), X38, .(T27, T30), T9, T31) → U2_gaaga(T27, T28, X38, T30, T9, T31, pA_in_gaaga(T28, X38, T30, T9, T31))
U2_gaaga(T27, T28, X38, T30, T9, T31, pA_out_gaaga(T28, X38, T30, T9, T31)) → pA_out_gaaga(.(T27, T28), X38, .(T27, T30), T9, T31)
U3_gaa(T8, T9, T12, T13, pA_out_gaaga(T8, X13, T12, T9, T13)) → flB_out_gaa(.(T8, T9), T12, s(T13))
FLB_IN_GAA(.(T8, T9), T12, s(T13)) → PA_IN_GAAGA(T8, X13, T12, T9, T13)
PA_IN_GAAGA([], T19, T19, T9, T20) → FLB_IN_GAA(T9, T19, T20)
PA_IN_GAAGA(.(T27, T28), X38, .(T27, T30), T9, T31) → PA_IN_GAAGA(T28, X38, T30, T9, T31)
flB_in_gaa([], [], 0) → flB_out_gaa([], [], 0)
flB_in_gaa(.(T8, T9), T12, s(T13)) → U3_gaa(T8, T9, T12, T13, pA_in_gaaga(T8, X13, T12, T9, T13))
pA_in_gaaga([], T19, T19, T9, T20) → U1_gaaga(T19, T9, T20, flB_in_gaa(T9, T19, T20))
U1_gaaga(T19, T9, T20, flB_out_gaa(T9, T19, T20)) → pA_out_gaaga([], T19, T19, T9, T20)
pA_in_gaaga(.(T27, T28), X38, .(T27, T30), T9, T31) → U2_gaaga(T27, T28, X38, T30, T9, T31, pA_in_gaaga(T28, X38, T30, T9, T31))
U2_gaaga(T27, T28, X38, T30, T9, T31, pA_out_gaaga(T28, X38, T30, T9, T31)) → pA_out_gaaga(.(T27, T28), X38, .(T27, T30), T9, T31)
U3_gaa(T8, T9, T12, T13, pA_out_gaaga(T8, X13, T12, T9, T13)) → flB_out_gaa(.(T8, T9), T12, s(T13))
FLB_IN_GAA(.(T8, T9), T12, s(T13)) → PA_IN_GAAGA(T8, X13, T12, T9, T13)
PA_IN_GAAGA([], T19, T19, T9, T20) → FLB_IN_GAA(T9, T19, T20)
PA_IN_GAAGA(.(T27, T28), X38, .(T27, T30), T9, T31) → PA_IN_GAAGA(T28, X38, T30, T9, T31)
FLB_IN_GAA(.(T8, T9)) → PA_IN_GAAGA(T8, T9)
PA_IN_GAAGA([], T9) → FLB_IN_GAA(T9)
PA_IN_GAAGA(.(T27, T28), T9) → PA_IN_GAAGA(T28, T9)
From the DPs we obtained the following set of size-change graphs: